perm filename REVERS.LSP[F85,JMC] blob
sn#806963 filedate 1985-11-08 generic text, type C, neo UTF8
COMMENT ⊗ VALID 00002 PAGES
C REC PAGE DESCRIPTION
C00001 00001
C00002 00002 revers.lsp[f85,jmc] Reverse stuff for ekl
C00003 ENDMK
C⊗;
;revers.lsp[f85,jmc] Reverse stuff for ekl
(get-proofs lispax prf prf jk)
(decl reverse (type: |ground → ground|)
(syntype: constant) (unaryname: reverse))
(defax reverse
|reverse nil = nil ∧ (∀x u. reverse (x.u) = reverse u * list(x))|)
(decl rev1 (type: |ground⊗ground → ground|) (syntype: constant))
(defax rev1 |(∀v.rev1(nil,v) = v) ∧ (∀x u v.rev1(x.u,v) = rev1(u,x.v))|)
(ue (phi |λu.listp reverse u|) listinduction (open reverse append))
(label simpinfo)
(ue (phi |λu.∀v.listp rev1(u,v)|) listinduction (open rev1))
(label simpinfo)
(save-proofs revers)